T:Type, R:(T
T
).
Trans(T;x,y.R(x,y))
{a, a', b, b':T.
Symmetrize(x,y.R(x,y);a;b) Symmetrize(x,y.R(x,y);a';b') (R(a,a') 
R(b,b'))} | 13,42 |
T:Type, R:(TT).
{a, a', b, b':T.
Symmetrize(x,y.R(x,y);a;b) Symmetrize(x,y.R(x,y);a';b') (R(a,a') R(b,b'))}
| Up | |
| Definitions |   x,y. t(x;y) T Q Q Qx:A. B(x) |
| Lemmas |